the proof LISP:

(DECL (U V W) |GROUND| VARIABLE LIST)

(DECL (X Y Z) |GROUND| VARIABLE SEXP)

(DECL (A B C) |GROUND| VARIABLE)

(DECL (PHI) |GROUND→TRUTHVAL| VARIABLE)

(DECL (NNIL) |GROUND| CONSTANT LIST)

(DECL (CONS) |GROUND⊗GROUND→GROUND| CONSTANT)

(DECL (CAR CDR) |GROUND→GROUND| CONSTANT)

(DECL (NULL) |GROUND→TRUTHVAL| CONSTANT)

(DECL (LIST) |GROUND→TRUTHVAL| CONSTANT)

(DECL (SEXP) |GROUND→TRUTHVAL| CONSTANT)

(AXIOM |∀U.SEXP(U)|)
11. ∀U.SEXP(U)
    ctxt: (1 10)   deps: NIL

(AXIOM |∀X U.LIST(CONS(X,U))|)
12. ∀X U.LIST(CONS(X,U))
    ctxt: (1 2 6 9)   deps: NIL

(AXIOM |∀U.NULL(U)≡U=NNIL|)
13. ∀U.NULL(U)≡U=NNIL
    ctxt: (1 5 8)   deps: NIL

(AXIOM |∀X U.¬NULL(CONS(X,U))|)
14. ∀X U.¬NULL(CONS(X,U))
    ctxt: (1 2 6 8)   deps: NIL

(AXIOM |∀X U.CAR(CONS(X,U))=X|)
15. ∀X U.CAR(CONS(X,U))=X
    ctxt: (1 2 6 7)   deps: NIL

(AXIOM |∀X U.CDR(CONS(X,U))=U|)
16. ∀X U.CDR(CONS(X,U))=U
    ctxt: (1 2 6 7)   deps: NIL

(AXIOM |∀PHI.PHI(NNIL)∧(∀X U.PHI(U)⊃PHI(CONS(X,U)))⊃(∀U.PHI(U))|)
17. ∀PHI.PHI(NNIL)∧(∀X U.PHI(U)⊃PHI(CONS(X,U)))⊃(∀U.PHI(U))
    ctxt: (1 2 4 5 6)   deps: NIL